In object-oriented software, objects often define usage protocols that clients must follow in order for these objects to work properly. Protocols essentially define legal sequences of method calls. In conventional object-oriented languages, developers have at least three ways of finding out about protocols: reading informal documentation, receiving runtime exceptions that indicate protocol violations, or observing incorrect program behavior as a result of protocol violations that broke internal invariants.
Aliasing, i.e., the existence of multiple references to the same object, is a significant complication in checking whether clients observe a protocol: a client does not necessarily know whether its reference to an object is the only reference that is active at a particular execution point. This also makes it difficult to check whether a class implements its specified protocol because reentrant callbacks through aliases can again lead to unexpected state changes.
Existing protocol checking approaches fall into two categories. They either operate globally, i.e., check an entire code base at once, or severely restrict aliasing. Global analyses typically account for aliasing, but they are not suitable for interactive use during development. Moreover, they do not check whether a declared protocol is implemented correctly, a crucial requirement in object-oriented software where any class might have a protocol of its own.
Modular protocol checkers, like Fugue [12], the first sound modular typestate checker for an object-oriented language, better support developers while they write code: like a typechecker, they check each method separately for protocol violations while assuming the rest of the system to behave as specified. The trade-off, unfortunately, has been that modular checkers require code to follow pre-defined patterns of aliasing. Once a program leaves the realm of supported aliasing, any further state changes are forbidden. Generally speaking, state changes are only allowed where the checker is aware of all references to the changing object.
This approach has serious drawbacks. First, many examples of realistic code might be excluded. Moreover, from a developer's point of view, the boundaries of what a checker supports are hard to predict, and they might not fit with the best implementation strategy for a particular problem. Finally, aliasing restrictions arguably leave developers alone just when they have the most trouble in reasoning about their code, namely, in the presence of subtle aliasing. Thus, a need exists for a method of checking an object-oriented program module having objects having multiple references by code not available for analysis.